// ***** This file is automatically generated from PairwiseLinearBinary.java.jpp

package daikon.inv.binary.twoSequence;

import daikon.*;
import daikon.inv.*;
import daikon.inv.DiscardInfo;
import daikon.inv.DiscardCode;
import daikon.inv.binary.twoScalar.*;
import daikon.Quantify.QuantFlags;
import java.util.*;

/**
 * Represents a linear invariant (i.e., <samp>y = ax + b</samp>) between
 * the corresponding elements of two sequences of double values.
 * Each <samp>(x[i], y[i])</samp> pair is examined.
 * Thus, <samp>x[0]</samp> is compared to <samp>y[0]</samp>,
 * <samp>x[1]</samp> to <samp>y[1]</samp> and so forth.
 * Prints as <samp>y[] = a * x[] + b</samp>.
 **/
public class PairwiseLinearBinaryFloat
  extends TwoSequenceFloat
{
  // We are Serializable, so we specify a version to allow changes to
  // method signatures without breaking serialization.  If you add or
  // remove fields, you should change this number to the current date.
  static final long serialVersionUID = 20030822L;

  // Variables starting with dkconfig_ should only be set via the
  // daikon.config.Configuration interface.
  /**
   * Boolean.  True iff PairwiseLinearBinary invariants should be considered.
   **/
  public static boolean dkconfig_enabled = true;

  public LinearBinaryCoreFloat core;

  @SuppressWarnings("nullness") // circular initialization
  protected PairwiseLinearBinaryFloat(PptSlice ppt) {
    super(ppt);
    core = new LinearBinaryCoreFloat(this);
  }

  @SuppressWarnings("nullness") // circular initialization
  protected /*@Prototype*/ PairwiseLinearBinaryFloat() {
    super();
    // Do we need a core in a prototype invariant?
    core = new LinearBinaryCoreFloat(this);
  }

  private static /*@Prototype*/ PairwiseLinearBinaryFloat proto;

  /** Returns the prototype invariant for PairwiseLinearBinaryFloat **/
  public static /*@Prototype*/ PairwiseLinearBinaryFloat get_proto() {
    if (proto == null)
      proto = new /*@Prototype*/ PairwiseLinearBinaryFloat ();
    return (proto);
  }

  /** Returns whether or not this invariant is enabled **/
  public boolean enabled() {
    return dkconfig_enabled;
  }

  /** Instantiates the invariant on the specified slice **/
  protected PairwiseLinearBinaryFloat instantiate_dyn (PptSlice slice) /*@Prototype*/ {
    return new PairwiseLinearBinaryFloat (slice);
  }

  public PairwiseLinearBinaryFloat clone() {
    PairwiseLinearBinaryFloat result = (PairwiseLinearBinaryFloat) super.clone();
    result.core = core.clone();
    result.core.wrapper = result;
    return result;
  }

  protected Invariant resurrect_done_swapped() {
    core.swap();
    return this;
  }

  public String repr() {
    return "PairwiseLinearBinaryFloat" + varNames() + ": "
      + "falsified=" + falsified
      + "; " + core.repr();
  }

  public String format_using(OutputFormat format) {
    if (core.a == 0 && core.b == 0 && core.c == 0) {
      return format_too_few_samples(format, null);
    }

    if (format == OutputFormat.DAIKON) return format_daikon();
    //if (format == OutputFormat.JML) return format_jml();
    if (format == OutputFormat.SIMPLIFY) return format_simplify();

    return format_unimplemented(format);
  }

  public String format_daikon() {
    return core.format_using(OutputFormat.DAIKON, var1().name(),
                             var2().name());
  }

  public String format_simplify() {
    String[] form = VarInfo.simplify_quantify (QuantFlags.element_wise(),
                                               var1(), var2());
    return form[0] + LinearBinaryCoreFloat.format_simplify(form[1], form[2],
                                               core.a, core.b, core.c)
      + form[3];
  }

  public InvariantStatus check_modified(double[] x_arr, double[] y_arr, int count) {
    return clone().add_modified(x_arr, y_arr, count);
  }

  public InvariantStatus add_modified(double[] x_arr, double[] y_arr, int count) {
    if (x_arr.length != y_arr.length) {
      return InvariantStatus.FALSIFIED;
    }
    int len = x_arr.length;
    // int len = Math.min(x_arr.length, y_arr.length);

    for (int i=0; i<len; i++) {
      double x = x_arr[i];
      double y = y_arr[i];

      if (core.add_modified(x, y, count) == InvariantStatus.FALSIFIED) {
        return InvariantStatus.FALSIFIED;
      }
    }
    return InvariantStatus.NO_CHANGE;
  }

  protected double computeConfidence() {
    return core.computeConfidence();
  }

  public boolean isSameFormula(Invariant other) {
    return core.isSameFormula(((PairwiseLinearBinaryFloat) other).core);
  }

  public boolean isExclusiveFormula(Invariant other) {
    if (other instanceof PairwiseLinearBinaryFloat) {
      return core.isExclusiveFormula(((PairwiseLinearBinaryFloat) other).core);
    }
    return false;
  }

  public /*@Nullable*/ DiscardInfo isObviousDynamically(VarInfo[] vis) {
    DiscardInfo super_result = super.isObviousDynamically(vis);
    if (super_result != null) {
      return super_result;
    }

    if (core.a == 0) {
      return new DiscardInfo(this, DiscardCode.obvious, var2().name() + " is constant");
    }
    if (core.b == 0) {
      return new DiscardInfo(this, DiscardCode.obvious, var1().name() + " is constant");
    }
//    if (core.a == 1 && core.b == 0) {
//      return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal");
//    }
    if (core.a == -core.b && core.c == 0) {
     return new DiscardInfo(this, DiscardCode.obvious, "Variables are equal");
    }
    return null;
  }

  public boolean isActive() {
    return core.isActive();
  }

  public boolean mergeFormulasOk() {
    return (core.mergeFormulasOk());
  }

  /**
   * Merge the invariants in invs to form a new invariant.  Each must be
   * a PairwiseLinearBinaryFloat invariant.  The work is done by the LinearBinary core
   *
   * @param invs        List of invariants to merge.  They should all be
   *                    permuted to match the variable order in parent_ppt.
   * @param parent_ppt  Slice that will contain the new invariant
   */
  public /*@Nullable*/ Invariant merge (List<Invariant> invs, PptSlice parent_ppt) {

    // Create a matching list of cores
    List<LinearBinaryCoreFloat> cores = new ArrayList<LinearBinaryCoreFloat>();
    for (Invariant inv : invs) {
      cores.add (((PairwiseLinearBinaryFloat) inv).core);
    }

    // Merge the cores and build a new invariant containing the merged core
    PairwiseLinearBinaryFloat result = new PairwiseLinearBinaryFloat (parent_ppt);
    LinearBinaryCoreFloat newcore = core.merge (cores, result);
    if (newcore == null)
      return (null);
    result.core = newcore;
    return (result);
  }

}
